feat(CategoryTheory/Sites): local sites#41083
Conversation
PR summary 335f3bdcb4Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (strong) |
|---|---|---|
| 4524 | 1 | backward.defeqAttrib.useBackward |
Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 4982 | 1 | exposed public sections |
Current commit 335f3bdcb4
Reference commit 8a9a2284f0
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
Now that we have an API for fiber functors, I think we should use it. noncomputable def LocalSite.point
[LocallySmall.{w} C] [J.IsLocalSite] : Point.{w} J :=
Point.ofIsCofiltered (N := Discrete (PUnit.{w + 1}))
(Discrete.functor (fun _ ↦ ⊤_ C)) (by
rintro X S hS ⟨⟨⟩⟩ (f : ⊤_ C ⟶ X)
exact ⟨_, _, LocalSite.from_terminal_mem_of_mem J f hS, ⟨.unit⟩, 𝟙 _, 𝟙 _, by simp⟩)The corresponding fiber functor identifies to the global section functors, and the right adjoint functor (the skyscraper sheaf functor) is defined in |
joelriou
added
the
awaiting-author
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on:
|
Co-authored-by: Christian Merten <christian@merten.dev>
| @[simp] | ||
| lemma productUniqueIso_hom [Unique β] (f : β → C) : (productUniqueIso f).hom = Pi.π f default := | ||
| rfl | ||
|
|
There was a problem hiding this comment.
Split PR created and commented
Split off the changes to Mathlib/CategoryTheory/Limits/Shapes/Products.lean in #41202 and posted a comment via splice-bot command maintainer.
3 participants
A local site is a site with a terminal object whose only covering sieve is the trivial one. We define local sites, construct a functor
coconstantSheafon them that is right-adjoint to the global sections functor, and prove that this functor and hence also the constant sheaf functor are fully faithful.A previous iteration of this was in #22817 already, but never got merged; this PR is based not directly on that version but on https://peabrainiac.github.io/lean-catdg/docs/CatDG/ForMathlib/LocalSite.html which I had developed a bit more since. Not all features from that file are included here to keep the PR small (in particular, I've left out the construction of the
localTopologyand proof that a site is local iff it is contained in that), but I did include some naming changes andIsLocalSite.tfaewhich was not in the previous PR.Another difference is that
Presheaf.coconstis now constructed explicitly instead of as a composition of several standard functors. @chrisflav I briefly asked you about this earlier, and you said that you preferred the construction as a composition, but after trying both approaches I came to the conclusion that the explicit approach is a lot more workable - the reason for this is thatPresheaf.coconst.obj Asends each objectXof the site to the type of functions(⊤_ C ⟶ X) → A, and it is important to be able to work with these functions explicitly. DefiningPresheaf.coconstin terms ofyonedaandcoyonedapreviously worked for this because morphism types inTypewere defeq to function types, but since a recent refactor they aren't anymore, which adds yet another source of friction in addition to the twoULifts that that definition inserts. I think even though that definition was elegant/nice, it is more important thatPresheaf.coconstevaluates up to defeq to types of functions and not morphism types involving twoULifts.shrinkCoyoneda#41150